◀ Prev · Parts · Full

layout: Wide · Narrow · Centered

• TACO, an open source program analysis tool that statically checks the

compliance of a Java program against its Java Modeling Language

specification.

• Gary T. Leavens and Yoonsik Cheon. Design by Contract with JML; Draft

tutorial.

• Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A Notation for

Detailed Design; in Haim Kilov, Bernhard Rumpe, and Ian Simmonds

(editors), Behavioral Specifications of Businesses and Systems, Kluwer,

1999, chapter 12, pages 175-188.

• Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby,

David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, and Daniel M.

Zimmerman. JML Reference Manual (DRAFT), September 2009. HTML

• Marieke Huisman, Wolfgang Ahrendt, Daniel Bruns, and Martin Hentschel.

Formal specification with JML. 2014. download (CC-BY-NC-ND)

• JML website

◀ Prev · Parts · Full